package edu.pku.sei.scriptengine.visitor;

import edu.pku.sei.mdabase.basictypes.OCLInvalid;
import edu.pku.sei.mdabase.basictypes.OCLVoidValue;
import edu.pku.sei.mdabase.infrastructure.runtime.Context;
import edu.pku.sei.mdabase.infrastructure.runtime.Variable;
import edu.pku.sei.queryscript.parser.Ast.AndExpr;
import edu.pku.sei.queryscript.parser.Ast.AtomicVariableExpr;
import edu.pku.sei.queryscript.parser.Ast.EqualExpr;
import edu.pku.sei.queryscript.parser.Ast.IfElseState;
import edu.pku.sei.queryscript.parser.Ast.IfState;
import edu.pku.sei.queryscript.parser.Ast.MinusExpr;
import edu.pku.sei.queryscript.parser.Ast.NotExpr;
import edu.pku.sei.queryscript.parser.Ast.OrExpr;
import edu.pku.sei.queryscript.parser.Ast.ParenQueryExpr;
import edu.pku.sei.queryscript.parser.Ast.PlusExpr;
import edu.pku.sei.queryscript.parser.Ast.QueryState;
import edu.pku.sei.queryscript.parser.Ast.RelationalArithExpr;



public class ModelCheckVisitor extends ExpressionCheckVisitor {

	
	public ModelCheckVisitor(Context context) {
		super(context);
	}
	
	public ModelCheckVisitor() {
		super();
	}
	
	@Override
	public Object visit(IfState n) {
		if(n.getLogicExpr().accept(this).equals(Boolean.TRUE)) {
			Object obj = n.getStatements().accept(this);
			history.commitAll();
			return obj;
		} else {
			history.restoreUncommit();
			return OCLVoidValue.NULL_VALUE;
		}
		
	}
	@Override
	public Object visit(IfElseState n) {
		if(n.getLogicExpr().accept(this).equals(Boolean.TRUE)) {
			Object obj =  n.getThenStatements().accept(this);
			history.commitAll();
			return obj;
		} else {
			Object obj = n.getElseStatements().accept(this);
			history.commitAll();
			return obj;
		}
	}
	
	
	@Override
	public Object visit(QueryState n) {
		Object obj =  n.getQueryExpr().accept(this);
		history.commitAll();
		return obj;
		
	}
	
	@Override
	public Object visit(EqualExpr n) {
		return n.accept(this, Boolean.TRUE);
	}
	
	@Override
	public Object visit(EqualExpr n, Object o) {
		//check first
		QueryVisitor checkVisitor = new ExpressionCheckVisitor();
		checkVisitor.copyEnvironment(this);
		//check result
		Object checkResult = n.accept(checkVisitor);
		//get value of left expression
		Object left = n.getLeftArithExpr().accept(checkVisitor);
		//get value of right expression
		Object right = n.getRightArithExpr().accept(checkVisitor);
		
		//check result equals to expected value
		if (checkResult.equals(o)) {
			return checkResult;
		} 
		//expected value is false, we don't know how to enforce
		//so don't do anything, and return check result
		else if (o.equals(Boolean.FALSE)) {
			return checkResult;
		} 
		//expected value is true
		else { 
			//neither side is void
			//we can't change un-void value, so return check result 
			if (!left.equals(OCLVoidValue.VOID) && !right.equals(OCLVoidValue.VOID)) {
				return checkResult;
			}
			//left side is binded a value, but right not
			//bind left value to right
			//check again and return result
			else if (!left.equals(OCLVoidValue.VOID)) {
				n.getRightArithExpr().accept(this, left);
				return n.accept(checkVisitor);
			} 
			//right side is binded a value, but left side not
			//bind right value to left
			//check again and return result
			else if (!right.equals(OCLVoidValue.VOID)) {
				n.getLeftArithExpr().accept(this, right);
				return n.accept(checkVisitor);
			} 
			//both sides are un-binded
			else {
				return checkResult;
			}
		}
	}
	
	@Override
	public Object visit(PlusExpr n, Object o) {
		//check first
		QueryVisitor checkVisitor = new ExpressionCheckVisitor();
		checkVisitor.copyEnvironment(this);
		Object left = n.getArithExpr().accept(checkVisitor);
		Object right = n.getAtomicExpr().accept(checkVisitor);
		Object checkResult = n.accept(checkVisitor);
		
		//if result equals expected result
		//return result
		if (checkResult.equals(o)) {
			return checkResult;
		}
		//can not bind
		else if (left == OCLVoidValue.VOID && right == OCLVoidValue.VOID) {
			return checkResult;
		}
		//bind value to left side
		else if (left == OCLVoidValue.VOID) {
			//both integer
			if (right instanceof Integer && o instanceof Integer) {
				n.getArithExpr().accept(this, ((Integer)o).intValue()-((Integer)right).intValue());
			} 
			//string (integer value should convert to string)
			else if (o instanceof String) {
				String s = right.toString();
				int index = ((String)o).lastIndexOf(s);
				if (((String) o).endsWith(s) && index != -1) {
					n.getArithExpr().accept(this, ((String)o).substring(0, index));
				} 
			}
		}
		//bind value to right side
		else if (right == OCLVoidValue.VOID) {
			//both integer
			if (left instanceof Integer && o instanceof Integer) {
				n.getAtomicExpr().accept(this, ((Integer)o).intValue() - ((Integer)left).intValue());
			} 
			//string 
			else if (o instanceof String) {
				String s = left.toString();
				if (((String) o).startsWith(s)) {
					n.getAtomicExpr().accept(this, ((String)o).substring(s.length()));
				} 
			}
		}
		//check again and return value
		checkResult = n.accept(checkVisitor);
		return checkResult;
	}
	
	@Override
	public Object visit(MinusExpr n, Object o) {
		//check first
		QueryVisitor checkVisitor = new ExpressionCheckVisitor();
		checkVisitor.copyEnvironment(this);
		Object left = n.getArithExpr().accept(checkVisitor);
		Object right = n.getAtomicExpr().accept(checkVisitor);
		Object checkResult = n.accept(checkVisitor);
		
		//result equals to expected result
		if (checkResult.equals(o)) {
			return checkResult;
		}
		//can not binding
		else if (left == OCLVoidValue.VOID && right == OCLVoidValue.VOID) {
			return checkResult;
		}
		//binding value to left side
		else if (left == OCLVoidValue.VOID) {
			//integer
			if (right instanceof Integer && o instanceof Integer) {
				left = n.getArithExpr().accept(this, ((Integer)o).intValue()+((Integer)right).intValue());
			}
			//do not support string kind minus
			/* else if (o instanceof String) {
				left = n.getArithExpr().accept(this, ((String)o)+right.toString());
			}*/
		}
		//bind value to right side
		else if (right == OCLVoidValue.VOID) {
			if (left instanceof Integer && o instanceof Integer) {
				right = n.getAtomicExpr().accept(this, ((Integer)left).intValue()-((Integer)o).intValue());
			}
			/*else if (o instanceof String) {
				String s = left.toString();
				if (((String) o).startsWith(s)) {
					right =n.getAtomicExpr().accept(this, ((String)o).substring(s.length()));
				} else {
					return OCLInvalid.invalid;
				}
			}*/
		}
		

		checkResult = n.accept(checkVisitor);
		return checkResult;
		
	}

	@Override
	public Object visit(AtomicVariableExpr n, Object o) {
		String  variableName = (String) n.getVariableExpr().accept(this);
		Object variable = getVariableByName(variableName);
		
		if (variable != null && variable instanceof Variable) {
			if (history.getValue(variable).equals(OCLVoidValue.VOID)) {
				if (history.setValue(variable, o))
					return o;
				else
					return history.getValue(variable);
			} else {
				return history.getValue(variable);
			}
		}
		else
			return OCLInvalid.INVALID;
	}
	
	@Override
	public Object visit(AndExpr n, Object o) {
		QueryVisitor checkVisitor = new ExpressionCheckVisitor();
		checkVisitor.copyEnvironment(this);
		Object left = n.getLogicExpr().accept(checkVisitor);
		Object right = n.getRelationalExpr().accept(checkVisitor);
		Object checkResult = n.accept(checkVisitor);
		
		if (o.equals(checkResult)) {
			return checkResult;
		} else if (o.equals(Boolean.FALSE)) {
			return checkResult;
		} else if (o.equals(Boolean.TRUE)) {
			if (left.equals(Boolean.TRUE)) {
				right = n.getRelationalExpr().accept(this, Boolean.TRUE);
			} else {
				left =  n.getLogicExpr().accept(this, true);
				if (left.equals(Boolean.TRUE)) {
					right = n.getRelationalExpr().accept(this,true);
				}		
			}
		} 
		return n.accept(checkVisitor);
	}
	
	@Override
	public Object visit(OrExpr n, Object o) {
		QueryVisitor checkVisitor = new ExpressionCheckVisitor();
		checkVisitor.copyEnvironment(this);
		Object left = n.getLogicExpr().accept(checkVisitor);
		Object right = n.getRelationalExpr().accept(checkVisitor);
		Object result = n.accept(checkVisitor);
		
		if (result.equals(o)) {
			return result;
		} else if (o.equals(Boolean.FALSE)) {
			return result;
		} else if (o.equals(Boolean.TRUE)) {
			if (left instanceof Boolean) {
				if (left.equals(Boolean.FALSE)) {
					if (!right.equals(Boolean.TRUE)) {
						right = n.getRelationalExpr().accept(this, Boolean.TRUE);
					}
				}
			} else {
				left = n.getLogicExpr().accept(this, Boolean.TRUE);
				if (!left.equals(Boolean.TRUE)) {
					if (!right.equals(Boolean.TRUE)) {
						right = n.getRelationalExpr().accept(this, Boolean.TRUE);
					}
				}
			}
		} 
			
		return n.accept(checkVisitor);
	}
	
	@Override
	public Object visit(NotExpr n, Object o) {
		QueryVisitor checkVisitor = new ExpressionCheckVisitor();
		checkVisitor.copyEnvironment(this);
		Object result = n.getRelationalExpr().accept(checkVisitor);
		
		if (result.equals(o)) {
			return result;
		} else if (result instanceof Boolean) {
			if (result.equals(Boolean.TRUE) && o.equals(Boolean.TRUE)) {
				n.getRelationalExpr().accept(this, Boolean.FALSE);
			} else if (result.equals(Boolean.FALSE) && o.equals(Boolean.FALSE)) {
				n.getRelationalExpr().accept(this, Boolean.TRUE);
			} 
		} else if (result == OCLVoidValue.VOID) {
			if (o.equals(Boolean.TRUE)) {
				n.getRelationalExpr().accept(this, Boolean.FALSE);
			} else if (o.equals(Boolean.FALSE)) {
				n.getRelationalExpr().accept(this, Boolean.TRUE);
			} 
		}
		
		result = n.getRelationalExpr().accept(checkVisitor);
		return result;
	}
	
	@Override
	public Object visit(ParenQueryExpr n, Object o) {
		return n.getQueryExpr().accept(this, o);
	}
	
	@Override
	public Object visit(RelationalArithExpr n, Object o) {
		return n.getArithExpr().accept(this, o);
	}
	
		
}
